Nuprl Definition : combine-ecl-tuples2 11,40

combine-ecl-tuples2(ABfg)
== spreadn(A;
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(B;
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(Tb,ksb,ib,gb,hb,ab,eb.<:Ta  (:Tb  (?))
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, append(ksaksb)
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, <iaib, inr  >
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(k',s,v,x. let sa = if deq-member(Kind-deq; k'ksa)
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, k',s,v,x. let then ga(k',s,v,x.1)
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, k',s,v,x. let else x.1
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, k',s,v,x. let fi  in
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, k',s,v,x. let flet sb = if deq-member(Kind-deq; k'ksb)
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, k',s,v,x. let flet then gb(k',s,v,(x.2).1)
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, k',s,v,x. let flet else (x.2).1
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, k',s,v,x. let flet fi  in
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, k',s,v,x. let flet f<sa
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, k',s,v,x. let flet sb
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, k',s,v,x. let flet , combine-halt-info(ea;
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, k',s,v,x. let flet , combine-halt-info(eb;
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, k',s,v,x. let flet , combine-halt-info((m.ha(m,sa));
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, k',s,v,x. let flet , combine-halt-info((m.hb(m,sb));
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, k',s,v,x. let flet , combine-halt-info((x.2.2))>
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(n,xf((x.2.2),m.ha(m,x.1),m.hb(m,(x.2).1),n)
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(n,k',s,v,xg
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, n,k',s,v,x(ha(0,x.1)
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, n,k',s,v,x,hb(0,(x.2).1)
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, n,k',s,v,x,reduce((m,b. bor((ha(m,x.1)); b)); ff; ea)
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, n,k',s,v,x,reduce((m,b. bor((hb(m,(x.2).1)); b));
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, n,k',s,v,x. ,reduce(ff;
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, n,k',s,v,x. ,reduce(eb)
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, n,k',s,v,x,if deq-member(Kind-deq; k'ksa)
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, n,k',s,v,x. ,then aa(n,k',s,v,x.1)
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, n,k',s,v,x. ,else ff
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, n,k',s,v,x. ,fi 
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, n,k',s,v,x,if deq-member(Kind-deq; k'ksb)
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, n,k',s,v,x. ,then ab(n,k',s,v,(x.2).1)
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, n,k',s,v,x. ,else ff
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, n,k',s,v,x. ,fi )
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, merge(eaeb)>)) 
latex



clarification:

combine-ecl-tuples2(ABfg)
== spreadn(A;
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(B;
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(Tb,ksb,ib,gb,hb,ab,eb.<:Ta  (:Tb  ( + Unit))
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, append(ksaksb)
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, <iaib, inr  >
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(k',s,v,x. let sa = if deq-member(Kind-deq; k'ksa)
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, k',s,v,x. let then ga(k',s,v,x.1)
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, k',s,v,x. let else x.1
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, k',s,v,x. let fi  in
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, k',s,v,x. let flet sb = if deq-member(Kind-deq; k'ksb)
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, k',s,v,x. let flet then gb(k',s,v,(x.2).1)
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, k',s,v,x. let flet else (x.2).1
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, k',s,v,x. let flet fi  in
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, k',s,v,x. let flet f<sa
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, k',s,v,x. let flet sb
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, k',s,v,x. let flet , combine-halt-info(ea;
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, k',s,v,x. let flet , combine-halt-info(eb;
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, k',s,v,x. let flet , combine-halt-info((m.ha(m,sa));
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, k',s,v,x. let flet , combine-halt-info((m.hb(m,sb));
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, k',s,v,x. let flet , combine-halt-info((x.2.2))>
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(n,xf((x.2.2),m.ha(m,x.1),m.hb(m,(x.2).1),n)
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(n,k',s,v,xg
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, n,k',s,v,x(ha(0,x.1)
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, n,k',s,v,x,hb(0,(x.2).1)
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, n,k',s,v,x,reduce((m,b. bor((ha(m,x.1)); b)); ff; ea)
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, n,k',s,v,x,reduce((m,b. bor((hb(m,(x.2).1)); b));
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, n,k',s,v,x. ,reduce(ff;
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, n,k',s,v,x. ,reduce(eb)
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, n,k',s,v,x,if deq-member(Kind-deq; k'ksa)
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, n,k',s,v,x. ,then aa(n,k',s,v,x.1)
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, n,k',s,v,x. ,else ff
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, n,k',s,v,x. ,fi 
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, n,k',s,v,x,if deq-member(Kind-deq; k'ksb)
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, n,k',s,v,x. ,then ab(n,k',s,v,(x.2).1)
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, n,k',s,v,x. ,else ff
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, n,k',s,v,x. ,fi )
== spreadn(Ta,ksa,ia,ga,ha,aa,ea.spreadn(, merge(eaeb)>)) 
latex


Definitionscombine-ecl-tuples2(ABfg), spreadn(ua,b,c,d,e,f,g.v(a;b;c;d;e;f;g)), , Unit, append(asbs), , let x = a in b(x), combine-halt-info(eaebfgx), reduce(fkas), bor(pq), if b then t else f fi , deq-member(eqxL), Kind-deq, t.1, t.2, ff, merge(asbs)
FDL editor aliasescombine-ecl-tuples2

origin